1. Field
This disclosure relates generally to integrated circuit logic design verification and, more specifically, to integrated circuit logic design verification techniques for liveness checking with retiming.
2. Related Art
In general, formal verification involves rigorously proving that an integrated circuit (IC) logic design (design) satisfies an associated specification. Typically, the specification of a verification problem includes a netlist representation of a design and a set of expected values for specified nets of the netlist. As an example, a verification problem may include determining whether a state exists in which a particular signal is asserted, where assertion of the particular signal indicates a fault. Using formal verification, an attempt is made to find a counter-example trace that includes a sequence of net values over time (states) that leads to an assertion of a particular signal or prove that no counter-example trace exists that leads to the assertion of the particular signal.
Formal verification is often performed using state space search algorithms, which include unbounded and bounded exhaustive search algorithms. Bounded exhaustive search algorithms attempt to find an assertion of a particular signal that occurs within ‘N’ time-steps from an initial state of a design. Unbounded exhaustive search algorithms increase ‘N’ until no states are encountered that have not already been encountered for smaller values of ‘N’ (a condition referred to as a ‘fixed-point’). If no path from an initial state to a violating state (i.e., a state in which the particular signal is asserted) is encountered before the fixed-point is reached, then correctness of a design can be inferred.
The number of verification cycles required to perform an exhaustive state space search increases exponentially with the number of state elements (e.g., registers, latches, flip-flops, etc.). This exponential relationship makes formal verification impractical for designs containing a large number of state elements (e.g., one-hundred or more state elements). As a result, semi-formal verification has been employed as a verification technique for large designs. Semi-formal verification leverages formal algorithms by applying the formal algorithms to larger designs in a resource-bounded manner. While requiring less computation time (as compared to formal verification), semi-formal verification may only achieve partial verification coverage.
Verification constraints (constraints) are constructs that may be employed in design verification applications. A constraint may be implemented as a specially-labeled gate (i.e., a constraint gate) in a netlist of a design. In general, a constraint represents a limitation on the freedom of a verification tool to explore a state space of a design. For example, a constraint may prevent a verification application from exploring any ‘j’ time-step trace in which any of one or more constraints evaluate to a logical zero during any of the ‘j’ time steps. Typically, a constraint defines a portion of a state space of a design that is irrelevant for verification purposes and, as such, would unnecessarily consume verification resources if the constraint were verified. As one example of a constraint, ‘a design may be constrained to prevent new transfers of data when a buffer is full’. In general, constraining inputs of the design to prohibit data transfers when the buffer is full means that a verification tool does not cover states that represent the design accepting new data transfers when the buffer is full.
In the absence of a constraint, a typical verification problem is stated as, for example, find a ‘j’ step trace that exhibits a violation of a property or prove that no such trace exists for any ‘j’. With a constraint, the same verification problem may be expressed as, for example, find a ‘j’ step trace that exhibits a violation of a property and does not exhibit a logical zero value for any constraint in any of the ‘j’ steps, or prove that no such trace exists for any ‘j’. Because constraints alter the semantics of a verification problem, constraints have the potential to cause a property that could be reached by a design to become unreachable. As such, it is desirable to select constraints judiciously. In general, constraints should not alter semantics of a verification problem. A constraint, for example, that would prevent a verification tool from discovering a valid assertion of a signal should not be permitted. Because constraints prohibit the exploration of certain otherwise reachable states, redundancy removal algorithms may leverage constraints to enable greater gate merging. In particular, redundancy removal algorithms may merge gates that are equivalent in all states reachable along paths that do not violate any constraints, even if the merged gates are not equivalent in some states that are reachable only after violating a constraint.
As previously mentioned, a verification tool operates on a model of a design known as a netlist. A netlist includes gates and edges, which represent interconnections between gates. A gate may, for example, fall into one of four broad functional categories: constant gates, random gates, combinational gates, and state elements (e.g., registers and sequential gates, such as latches and flip-flops). A constant gate produces a logic level that does not vary with time. A random gate (also referred to as a primary input) may assume any logic level in any time-step independent of all other gates. A combinational gate is a logical element such as an AND gate, an OR gate, a NAND gate, a NOR gate, etc. A sequential gate has an associated initial value function and a next state function. The value of a sequential gate at time ‘0’ (t0) is the value of the initial value function. The value of a sequential gate at time ‘i+1’ is equal to the value of the next state function of the sequential gate at time ‘i’.
A cutpoint gate may be introduced (into a modified netlist) by replacing a sequential gate in an original netlist with a random gate. An output of a random gate drives the same inputs in the modified netlist as an associated sequential gate drove in an original netlist. Unlike the inputs of the sequential gate in the original netlist, however, the inputs of the random gate are random inputs that are not connected to any other elements of the modified netlist. Inputs to a random gate can assume any value on any gate cycle irrespective of other stimulus applied to a design. As such, the net effect of introducing cutpoints into a netlist may be to over-approximate the behavior of a design, as a random gate can simulate behavior of the sequential gate, while the converse is not necessarily true. As an over-approximate model of an original netlist, a modified netlist may include states from which a target gate could not be asserted in the original netlist.
Retiming techniques, which were originally developed for enhanced synthesis, have more recently been proposed to enhance verification (i.e., reduce verification time) through reduction in latch (flip-flop) count. Generally speaking, retiming refers to the process of moving latches across combinational gates. In general, many prior art retiming algorithms have shifted every gate in a design under verification by an arbitrary amount, which may pose challenges to the use of retiming in a verification setting under the presence of constraints.
Liveness checking of a design refers to verification of properties (of the design), which are used to assess whether the design eventually behaves in a correct manner. For example, when verifying an arbiter, it may be desirable to check a property that, for example, states ‘every request presented to the arbiter is eventually granted’. Any counter-example trace to the property must be of infinite length to show a request that never receives a grant (i.e., an infinite length sequence of bad behavior). A counter-example trace is often represented using a finite-length trace, where some suffix of the trace (denoted by assertion of a specially-added LOOP signal (with a corresponding loop gate) added by a verification tool), which starts with a state and ends with the same state, may be infinitely repeated. For example, assuming that a trace runs from time ‘0’ (t0) to time ‘50’ (t50) and the LOOP signal is asserted at time ‘20’ (t20), an initial state of a design at time t20 must correspond to a final state of the design at time t50 for a valid counter-example for the suffix (which extends from times t20 to t50). Semantically, the finite-length trace represents an infinite length counter-example as suffix (loop) behavior may be repeated as many times as desired to provide a request without a grant scenario.
Liveness checking may be contrasted with safety checking, which may be represented by checking whether a given signal of a design is ever asserted to a logical one. In general, safety checking refers to design verification of a property that may be disproven in a finite amount of time. In contrast, liveness checking refers to design verification of a property that requires an infinite amount of time to disprove. Liveness checking for a design can be cast as safety checking for the design through a known transformation, which facilitates sampling a current state of the design and later checking for a repetition of the state which completes a behavioral loop. However, the known transformation effectively doubles state elements of the design during verification and, as such, adds substantial overhead to a verification process.